T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} .
x changed before e   

latex

Definitions	Type, t  T, x:A. B(x), EqDecider(T), event_system{i:l}, Id, loc(e), es-dtype(es; i; x; T), es-E(es), {x:A| B(x)} , change-to(x;e), Unit, isl(x), x changed before e
Lemmas	isl wf, unit wf, change-to wf, es-E wf, es-dtype wf, es-loc wf, Id wf, event system wf, deq wf